| Definitions | t  T, finite-prob-space, ternary-fps, P  Q, qsum(a; b; j.E(j)), ||as||, l[i], l_all(L; T; x.P(x)), qle(r; s), qdiv(r; s),  x:A. B(x), P   Q,  A, P  Q,  b, qeq(r; s), P Q, prop{i:l}, if b then t else f fi , tt, (i = j), ff, True, False, A c B,   x. t(x), A  B, rng_sum(r; i; j; k.E(k)), mon_itop(g; lb; ub; i.E(i)), itop(op; id; lb; ub; i.E(i)), Y, i <z j, x f y, grp_op(g), t.1, t.2, add_grp_of_rng(r), rng_plus(r), qrng, r + s, grp_id(g), rng_zero(r), hd(l), nth_tl(n;as), i z j,  b, r * s, qinv(r), tl(l), sq_type(T), guard(T), grp_leq(g; a; b), grp_le(g), qadd_grp, q_le(r; s), bor(p; q), qpositive(r), r - s, band(p; q), int_seg(i; j), x(s), lelt(i; j; k), (x l),  x:A. B(x),  , decidable(P), P  Q, subtype(S; T) |